(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 1))
(let ((e2 (- v0 v0)))
(let ((e3 (- v0 v0)))
(let ((e4 (- e2)))
(let ((e5 (+ e3 e3)))
(let ((e6 (- e4)))
(let ((e7 (+ v0 e3)))
(let ((e8 (- e2)))
(let ((e9 (- e2 e5)))
(let ((e10 (- v0 e4)))
(let ((e11 (* e8 (- e1))))
(let ((e12 (= e7 e9)))
(let ((e13 (<= e6 v0)))
(let ((e14 (< e7 e5)))
(let ((e15 (< e5 e7)))
(let ((e16 (>= e6 e8)))
(let ((e17 (>= e2 e8)))
(let ((e18 (= e5 e10)))
(let ((e19 (= e3 e4)))
(let ((e20 (>= v0 v0)))
(let ((e21 (= e5 e3)))
(let ((e22 (= e7 e3)))
(let ((e23 (distinct e4 e4)))
(let ((e24 (> v0 e6)))
(let ((e25 (distinct e4 e8)))
(let ((e26 (< e2 e8)))
(let ((e27 (distinct e4 e6)))
(let ((e28 (< e11 e3)))
(let ((e29 (ite e19 v0 e9)))
(let ((e30 (ite e18 e7 e29)))
(let ((e31 (ite e13 e6 e2)))
(let ((e32 (ite e25 e2 e4)))
(let ((e33 (ite e27 e3 e4)))
(let ((e34 (ite e24 e8 e9)))
(let ((e35 (ite e14 e11 e11)))
(let ((e36 (ite e26 e34 e10)))
(let ((e37 (ite e16 e5 e4)))
(let ((e38 (ite e15 e7 v0)))
(let ((e39 (ite e18 e32 v0)))
(let ((e40 (ite e22 e30 e36)))
(let ((e41 (ite e12 e37 e8)))
(let ((e42 (ite e23 e36 e36)))
(let ((e43 (ite e16 e10 e6)))
(let ((e44 (ite e16 e4 e36)))
(let ((e45 (ite e23 e34 e10)))
(let ((e46 (ite e26 e31 e30)))
(let ((e47 (ite e17 e11 e7)))
(let ((e48 (ite e20 e40 e40)))
(let ((e49 (ite e28 e33 e9)))
(let ((e50 (ite e21 e31 e29)))
(let ((e51 (= e39 e49)))
(let ((e52 (>= e7 e34)))
(let ((e53 (< e43 e2)))
(let ((e54 (>= e33 e43)))
(let ((e55 (< e41 e40)))
(let ((e56 (<= e2 e44)))
(let ((e57 (<= e29 e6)))
(let ((e58 (<= e43 e7)))
(let ((e59 (= e39 e33)))
(let ((e60 (< e30 e31)))
(let ((e61 (< e50 e8)))
(let ((e62 (>= e10 e2)))
(let ((e63 (< e10 e5)))
(let ((e64 (distinct e45 e4)))
(let ((e65 (> e10 e33)))
(let ((e66 (distinct e45 e6)))
(let ((e67 (> e10 e30)))
(let ((e68 (<= e38 e7)))
(let ((e69 (= e37 e39)))
(let ((e70 (<= e37 v0)))
(let ((e71 (>= e33 e50)))
(let ((e72 (distinct e40 e39)))
(let ((e73 (distinct e7 e34)))
(let ((e74 (= e37 e31)))
(let ((e75 (<= e44 e36)))
(let ((e76 (= e31 e30)))
(let ((e77 (> e42 e6)))
(let ((e78 (distinct e34 e44)))
(let ((e79 (<= e35 e30)))
(let ((e80 (<= e34 e39)))
(let ((e81 (distinct e44 e37)))
(let ((e82 (<= e3 e29)))
(let ((e83 (<= e7 e32)))
(let ((e84 (<= e34 e42)))
(let ((e85 (>= e43 e10)))
(let ((e86 (> e31 e45)))
(let ((e87 (>= e32 v0)))
(let ((e88 (distinct e4 e8)))
(let ((e89 (<= e47 e11)))
(let ((e90 (>= e46 e29)))
(let ((e91 (< e29 e3)))
(let ((e92 (= e36 e45)))
(let ((e93 (> e34 e7)))
(let ((e94 (> e36 e38)))
(let ((e95 (>= e41 e31)))
(let ((e96 (distinct e42 e37)))
(let ((e97 (>= e31 e6)))
(let ((e98 (= e6 e37)))
(let ((e99 (> e46 e32)))
(let ((e100 (<= e29 e33)))
(let ((e101 (>= e32 e41)))
(let ((e102 (= e32 e38)))
(let ((e103 (<= e49 e34)))
(let ((e104 (<= e39 e35)))
(let ((e105 (> e31 e50)))
(let ((e106 (>= e30 e11)))
(let ((e107 (>= e2 e33)))
(let ((e108 (= e35 e33)))
(let ((e109 (distinct e41 e41)))
(let ((e110 (distinct e42 e39)))
(let ((e111 (<= e44 e40)))
(let ((e112 (<= e43 e34)))
(let ((e113 (> e3 e33)))
(let ((e114 (= e49 e9)))
(let ((e115 (> e39 e37)))
(let ((e116 (>= e37 v0)))
(let ((e117 (<= e4 e30)))
(let ((e118 (distinct e11 e7)))
(let ((e119 (> e45 e46)))
(let ((e120 (> e40 e49)))
(let ((e121 (< e29 e44)))
(let ((e122 (< e3 e42)))
(let ((e123 (> e9 e45)))
(let ((e124 (= e7 e50)))
(let ((e125 (distinct e2 e5)))
(let ((e126 (= e50 e29)))
(let ((e127 (<= e50 e4)))
(let ((e128 (< e37 e50)))
(let ((e129 (< e32 e5)))
(let ((e130 (< e5 e31)))
(let ((e131 (>= e43 e34)))
(let ((e132 (distinct e35 e3)))
(let ((e133 (<= e30 e48)))
(let ((e134 (ite e116 e58 e116)))
(let ((e135 (and e53 e128)))
(let ((e136 (or e16 e60)))
(let ((e137 (xor e81 e85)))
(let ((e138 (or e92 e96)))
(let ((e139 (=> e64 e13)))
(let ((e140 (and e74 e115)))
(let ((e141 (and e24 e84)))
(let ((e142 (xor e139 e87)))
(let ((e143 (ite e15 e112 e126)))
(let ((e144 (and e73 e14)))
(let ((e145 (ite e52 e143 e70)))
(let ((e146 (and e131 e113)))
(let ((e147 (= e136 e28)))
(let ((e148 (or e109 e63)))
(let ((e149 (and e119 e59)))
(let ((e150 (ite e134 e75 e101)))
(let ((e151 (xor e71 e118)))
(let ((e152 (and e89 e147)))
(let ((e153 (and e110 e86)))
(let ((e154 (not e26)))
(let ((e155 (and e82 e22)))
(let ((e156 (and e123 e83)))
(let ((e157 (ite e117 e114 e55)))
(let ((e158 (and e154 e19)))
(let ((e159 (ite e88 e68 e108)))
(let ((e160 (xor e23 e133)))
(let ((e161 (not e151)))
(let ((e162 (= e65 e120)))
(let ((e163 (xor e97 e78)))
(let ((e164 (=> e156 e56)))
(let ((e165 (=> e111 e163)))
(let ((e166 (ite e152 e57 e69)))
(let ((e167 (=> e61 e20)))
(let ((e168 (=> e106 e77)))
(let ((e169 (=> e127 e129)))
(let ((e170 (xor e157 e91)))
(let ((e171 (xor e17 e138)))
(let ((e172 (and e72 e121)))
(let ((e173 (= e141 e155)))
(let ((e174 (or e79 e142)))
(let ((e175 (or e124 e21)))
(let ((e176 (ite e149 e170 e172)))
(let ((e177 (=> e80 e95)))
(let ((e178 (not e164)))
(let ((e179 (xor e159 e145)))
(let ((e180 (and e98 e135)))
(let ((e181 (ite e76 e104 e93)))
(let ((e182 (or e90 e66)))
(let ((e183 (=> e102 e94)))
(let ((e184 (and e125 e137)))
(let ((e185 (and e130 e162)))
(let ((e186 (or e140 e160)))
(let ((e187 (ite e107 e186 e99)))
(let ((e188 (=> e168 e148)))
(let ((e189 (xor e185 e183)))
(let ((e190 (= e18 e174)))
(let ((e191 (and e175 e188)))
(let ((e192 (=> e161 e158)))
(let ((e193 (and e27 e144)))
(let ((e194 (and e67 e192)))
(let ((e195 (= e51 e193)))
(let ((e196 (or e132 e54)))
(let ((e197 (not e187)))
(let ((e198 (ite e25 e12 e169)))
(let ((e199 (ite e167 e189 e190)))
(let ((e200 (not e165)))
(let ((e201 (or e182 e182)))
(let ((e202 (ite e166 e178 e179)))
(let ((e203 (or e199 e176)))
(let ((e204 (not e105)))
(let ((e205 (= e191 e180)))
(let ((e206 (or e153 e146)))
(let ((e207 (not e181)))
(let ((e208 (not e173)))
(let ((e209 (ite e122 e198 e197)))
(let ((e210 (or e100 e100)))
(let ((e211 (ite e62 e207 e206)))
(let ((e212 (and e195 e177)))
(let ((e213 (or e150 e209)))
(let ((e214 (and e200 e196)))
(let ((e215 (not e203)))
(let ((e216 (not e208)))
(let ((e217 (and e212 e204)))
(let ((e218 (ite e201 e184 e217)))
(let ((e219 (=> e214 e205)))
(let ((e220 (or e202 e218)))
(let ((e221 (not e194)))
(let ((e222 (not e216)))
(let ((e223 (xor e219 e213)))
(let ((e224 (ite e220 e211 e103)))
(let ((e225 (xor e222 e215)))
(let ((e226 (ite e210 e210 e210)))
(let ((e227 (or e226 e224)))
(let ((e228 (=> e221 e221)))
(let ((e229 (xor e228 e228)))
(let ((e230 (xor e171 e227)))
(let ((e231 (or e225 e225)))
(let ((e232 (not e223)))
(let ((e233 (ite e232 e229 e232)))
(let ((e234 (=> e231 e231)))
(let ((e235 (not e230)))
(let ((e236 (= e235 e234)))
(let ((e237 (not e236)))
(let ((e238 (or e237 e237)))
(let ((e239 (xor e233 e233)))
(let ((e240 (= e238 e239)))
e240
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
